c-refinement/tests/TakePut_TP.thy - 3p/nicta/cogent - Git at Google

 (*
  * Copyright 2016, NICTA
  *
  * This software may be distributed and modified according to the terms of
  * the GNU General Public License version 2. Note that NO WARRANTY is provided.
  * See "LICENSE_GPLv2.txt" for details.
  *
  * @TAG(NICTA_GPL)
  *)

 (*
   This file is generated by Cogent version 2.3.0.0-b3438dfb09
     with command ./cogent --type-proof=TakePut_TP --fml-typing-tree pass_simple-take-letput.cogent --fimports-in-typeproof=../TypeProof/Gen
     at Fri, 15 May 2015 16:47:17 AEST
 *)

 theory TakePut_TP
 imports "../TypeProofGen"
 begin

 definition
   "abbreviatedType1 \<equiv> TRecord [(TPrim (Num U8), False), (TPrim (Num U16), False)] Writable"

 definition
   "abbreviatedType2 \<equiv> TRecord [(TPrim (Num U16), False), (TPrim (Num U32), False)] Writable"

 lemmas abbreviated_type_defs =
   abbreviatedType2_def
   abbreviatedType1_def

 definition
   "foobar_type \<equiv> ([], (abbreviatedType2, abbreviatedType2))"

 definition
   "foobar \<equiv> Let (Var 0) (Take (Var 0) 0 (Let (Put (Var 1) 0 (Var 0)) (Var 0)))"

 definition
   "foo_type \<equiv> ([], (abbreviatedType1, abbreviatedType1))"

 definition
   "foo \<equiv> Let (Var 0) (Take (Var 0) 0 (Let (Put (Var 1) 0 (Var 0)) (Var 0)))"

 ML {*
 val Cogent_functions = ["foobar","foo"]
 val Cogent_abstract_functions = []
 *}

 definition
   "\<Xi> func_name' \<equiv> case func_name' of ''foobar'' \<Rightarrow> foobar_type | ''foo'' \<Rightarrow> foo_type"

 definition
   "foobar_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some abbreviatedType2] (TyTrSplit (Cons (Some TSK_L) (Cons None [])) [] TyTrLeaf [Some (TPrim (Num U16)), Some (TRecord [(TPrim (Num U16), True), (TPrim (Num U32), False)] Writable)] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 2 None) []))) [] TyTrLeaf [Some abbreviatedType2] TyTrLeaf))"

 definition
   "foo_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some abbreviatedType1] (TyTrSplit (Cons (Some TSK_L) (Cons None [])) [] TyTrLeaf [Some (TPrim (Num U8)), Some (TRecord [(TPrim (Num U8), True), (TPrim (Num U16), False)] Writable)] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 2 None) []))) [] TyTrLeaf [Some abbreviatedType1] TyTrLeaf))"

 ML {* open TTyping_Tactics *}

 ML_quiet {*
 val typing_helper_1_script : tac list = [
 (RTac @{thm kind_tprim})
 ] *}


 lemma typing_helper_1[unfolded abbreviated_type_defs] :
   "kinding [] (TPrim (Num U16)) {E}"
   apply (unfold abbreviated_type_defs)?
   apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_1_script |> EVERY *})
   done

 ML_quiet {*
 val typing_helper_2_script : tac list = [
 (RTac @{thm kind_tprim})
 ] *}


 lemma typing_helper_2[unfolded abbreviated_type_defs] :
   "kinding [] (TPrim (Num U32)) {E}"
   apply (unfold abbreviated_type_defs)?
   apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_2_script |> EVERY *})
   done

 ML_quiet {*
 val typing_helper_3_script : tac list = [
 (RTac @{thm kind_trec[where k = "{E}"]}),
 (RTac @{thm kind_record_cons1}),
 (RTac @{thm typing_helper_1}),
 (RTac @{thm kind_record_cons1}),
 (RTac @{thm typing_helper_2}),
 (RTac @{thm kind_record_empty}),
 (SimpTac ([],[]))
 ] *}


 lemma typing_helper_3[unfolded abbreviated_type_defs] :
   "kinding [] abbreviatedType2 {E}"
   apply (unfold abbreviated_type_defs)?
   apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_3_script |> EVERY *})
   done

 ML_quiet {*
 val typing_helper_4_script : tac list = [
 (RTac @{thm kind_tprim[where k = "{E,S,D}"]})
 ] *}


 lemma typing_helper_4[unfolded abbreviated_type_defs] :
   "kinding [] (TPrim (Num U16)) {E, S, D}"
   apply (unfold abbreviated_type_defs)?
   apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_4_script |> EVERY *})
   done

 ML_quiet {*
 val typing_helper_5_script : tac list = [
 (RTac @{thm kind_trec[where k = "{E}"]}),
 (RTac @{thm kind_record_cons2}),
 (RTac @{thm typing_helper_4}),
 (RTac @{thm kind_record_cons1}),
 (RTac @{thm typing_helper_2}),
 (RTac @{thm kind_record_empty}),
 (SimpTac ([],[]))
 ] *}


 lemma typing_helper_5[unfolded abbreviated_type_defs] :
   "kinding [] (TRecord [(TPrim (Num U16), True), (TPrim (Num U32), False)] Writable) {E}"
   apply (unfold abbreviated_type_defs)?
   apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_5_script |> EVERY *})
   done

 ML_quiet {*
 val typing_helper_6_script : tac list = [
 (RTac @{thm kind_tprim})
 ] *}


 lemma typing_helper_6[unfolded abbreviated_type_defs] :
   "kinding [] (TPrim (Num U8)) {E}"
   apply (unfold abbreviated_type_defs)?
   apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_6_script |> EVERY *})
   done

 ML_quiet {*
 val typing_helper_7_script : tac list = [
 (RTac @{thm kind_trec[where k = "{E}"]}),
 (RTac @{thm kind_record_cons1}),
 (RTac @{thm typing_helper_6}),
 (RTac @{thm kind_record_cons1}),
 (RTac @{thm typing_helper_1}),
 (RTac @{thm kind_record_empty}),
 (SimpTac ([],[]))
 ] *}


 lemma typing_helper_7[unfolded abbreviated_type_defs] :
   "kinding [] abbreviatedType1 {E}"
   apply (unfold abbreviated_type_defs)?
   apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_7_script |> EVERY *})
   done

 ML_quiet {*
 val typing_helper_8_script : tac list = [
 (RTac @{thm kind_tprim[where k = "{E,S,D}"]})
 ] *}


 lemma typing_helper_8[unfolded abbreviated_type_defs] :
   "kinding [] (TPrim (Num U8)) {E, S, D}"
   apply (unfold abbreviated_type_defs)?
   apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_8_script |> EVERY *})
   done

 ML_quiet {*
 val typing_helper_9_script : tac list = [
 (RTac @{thm kind_trec[where k = "{E}"]}),
 (RTac @{thm kind_record_cons2}),
 (RTac @{thm typing_helper_8}),
 (RTac @{thm kind_record_cons1}),
 (RTac @{thm typing_helper_1}),
 (RTac @{thm kind_record_empty}),
 (SimpTac ([],[]))
 ] *}


 lemma typing_helper_9[unfolded abbreviated_type_defs] :
   "kinding [] (TRecord [(TPrim (Num U8), True), (TPrim (Num U16), False)] Writable) {E}"
   apply (unfold abbreviated_type_defs)?
   apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_9_script |> EVERY *})
   done

 ML_quiet {*
 val foobar_typecorrect_script : hints list = [
 KindingTacs [(RTac @{thm typing_helper_3})],
 KindingTacs [(RTac @{thm typing_helper_3})],
 TypingTacs [],
 KindingTacs [(RTac @{thm typing_helper_4})],
 KindingTacs [(RTac @{thm typing_helper_5})],
 TypingTacs [],
 KindingTacs [(RTac @{thm typing_helper_4})],
 KindingTacs [(RTac @{thm typing_helper_3})],
 TypingTacs [(RTac @{thm typing_put'}),(SplitsTac (4,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_4})]),(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[@{thm Product_Type.prod.inject}])),(RTac @{thm typing_helper_4}),(RTac @{thm disjI2[where Q = "True"]}),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_4}]),(SimpTac ([],[])),(SimpTac ([],[]))],
 TypingTacs []
 ] *}


 ML_quiet {*
 val foobar_ttyping_details_future = get_all_typing_details_future @{context} "foobar"
    foobar_typecorrect_script*}


 lemma foobar_typecorrect :
   "\<Xi>, fst foobar_type, (foobar_typetree, [Some (fst (snd foobar_type))]) T\<turnstile> foobar : snd (snd foobar_type)"
   apply (tactic {* resolve_future_typecorrect @{context} foobar_ttyping_details_future *})
   done

 ML_quiet {*
 val foo_typecorrect_script : hints list = [
 KindingTacs [(RTac @{thm typing_helper_7})],
 KindingTacs [(RTac @{thm typing_helper_7})],
 TypingTacs [],
 KindingTacs [(RTac @{thm typing_helper_8})],
 KindingTacs [(RTac @{thm typing_helper_9})],
 TypingTacs [],
 KindingTacs [(RTac @{thm typing_helper_8})],
 KindingTacs [(RTac @{thm typing_helper_7})],
 TypingTacs [(RTac @{thm typing_put'}),(SplitsTac (4,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_8})]),(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_9})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_9}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[@{thm Product_Type.prod.inject}])),(RTac @{thm typing_helper_8}),(RTac @{thm disjI2[where Q = "True"]}),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_8}]),(SimpTac ([],[])),(SimpTac ([],[]))],
 TypingTacs []
 ] *}


 ML_quiet {*
 val foo_ttyping_details_future = get_all_typing_details_future @{context} "foo"
    foo_typecorrect_script*}


 lemma foo_typecorrect :
   "\<Xi>, fst foo_type, (foo_typetree, [Some (fst (snd foo_type))]) T\<turnstile> foo : snd (snd foo_type)"
   apply (tactic {* resolve_future_typecorrect @{context} foo_ttyping_details_future *})
   done

 ML_quiet {*
 val (_, foobar_typing_tree, foobar_typing_bucket)
 = Future.join foobar_ttyping_details_future
 *}


 ML_quiet {*
 val (_, foo_typing_tree, foo_typing_bucket)
 = Future.join foo_ttyping_details_future
 *}


 end
	(*
	* Copyright 2016, NICTA
	*
	* This software may be distributed and modified according to the terms of
	* the GNU General Public License version 2. Note that NO WARRANTY is provided.
	* See "LICENSE_GPLv2.txt" for details.
	*
	* @TAG(NICTA_GPL)
	*)

	(*
	This file is generated by Cogent version 2.3.0.0-b3438dfb09
	with command ./cogent --type-proof=TakePut_TP --fml-typing-tree pass_simple-take-letput.cogent --fimports-in-typeproof=../TypeProof/Gen
	at Fri, 15 May 2015 16:47:17 AEST
	*)

	theory TakePut_TP
	imports "../TypeProofGen"
	begin

	definition
	"abbreviatedType1 \<equiv> TRecord [(TPrim (Num U8), False), (TPrim (Num U16), False)] Writable"

	definition
	"abbreviatedType2 \<equiv> TRecord [(TPrim (Num U16), False), (TPrim (Num U32), False)] Writable"

	lemmas abbreviated_type_defs =
	abbreviatedType2_def
	abbreviatedType1_def

	definition
	"foobar_type \<equiv> ([], (abbreviatedType2, abbreviatedType2))"

	definition
	"foobar \<equiv> Let (Var 0) (Take (Var 0) 0 (Let (Put (Var 1) 0 (Var 0)) (Var 0)))"

	definition
	"foo_type \<equiv> ([], (abbreviatedType1, abbreviatedType1))"

	definition
	"foo \<equiv> Let (Var 0) (Take (Var 0) 0 (Let (Put (Var 1) 0 (Var 0)) (Var 0)))"

	ML {*
	val Cogent_functions = ["foobar","foo"]
	val Cogent_abstract_functions = []
	*}

	definition
	"\<Xi> func_name' \<equiv> case func_name' of ''foobar'' \<Rightarrow> foobar_type \| ''foo'' \<Rightarrow> foo_type"

	definition
	"foobar_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some abbreviatedType2] (TyTrSplit (Cons (Some TSK_L) (Cons None [])) [] TyTrLeaf [Some (TPrim (Num U16)), Some (TRecord [(TPrim (Num U16), True), (TPrim (Num U32), False)] Writable)] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 2 None) []))) [] TyTrLeaf [Some abbreviatedType2] TyTrLeaf))"

	definition
	"foo_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some abbreviatedType1] (TyTrSplit (Cons (Some TSK_L) (Cons None [])) [] TyTrLeaf [Some (TPrim (Num U8)), Some (TRecord [(TPrim (Num U8), True), (TPrim (Num U16), False)] Writable)] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 2 None) []))) [] TyTrLeaf [Some abbreviatedType1] TyTrLeaf))"

	ML {* open TTyping_Tactics *}

	ML_quiet {*
	val typing_helper_1_script : tac list = [
	(RTac @{thm kind_tprim})
	] *}


	lemma typing_helper_1[unfolded abbreviated_type_defs] :
	"kinding [] (TPrim (Num U16)) {E}"
	apply (unfold abbreviated_type_defs)?
	apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_1_script \|> EVERY *})
	done

	ML_quiet {*
	val typing_helper_2_script : tac list = [
	(RTac @{thm kind_tprim})
	] *}


	lemma typing_helper_2[unfolded abbreviated_type_defs] :
	"kinding [] (TPrim (Num U32)) {E}"
	apply (unfold abbreviated_type_defs)?
	apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_2_script \|> EVERY *})
	done

	ML_quiet {*
	val typing_helper_3_script : tac list = [
	(RTac @{thm kind_trec[where k = "{E}"]}),
	(RTac @{thm kind_record_cons1}),
	(RTac @{thm typing_helper_1}),
	(RTac @{thm kind_record_cons1}),
	(RTac @{thm typing_helper_2}),
	(RTac @{thm kind_record_empty}),
	(SimpTac ([],[]))
	] *}


	lemma typing_helper_3[unfolded abbreviated_type_defs] :
	"kinding [] abbreviatedType2 {E}"
	apply (unfold abbreviated_type_defs)?
	apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_3_script \|> EVERY *})
	done

	ML_quiet {*
	val typing_helper_4_script : tac list = [
	(RTac @{thm kind_tprim[where k = "{E,S,D}"]})
	] *}


	lemma typing_helper_4[unfolded abbreviated_type_defs] :
	"kinding [] (TPrim (Num U16)) {E, S, D}"
	apply (unfold abbreviated_type_defs)?
	apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_4_script \|> EVERY *})
	done

	ML_quiet {*
	val typing_helper_5_script : tac list = [
	(RTac @{thm kind_trec[where k = "{E}"]}),
	(RTac @{thm kind_record_cons2}),
	(RTac @{thm typing_helper_4}),
	(RTac @{thm kind_record_cons1}),
	(RTac @{thm typing_helper_2}),
	(RTac @{thm kind_record_empty}),
	(SimpTac ([],[]))
	] *}


	lemma typing_helper_5[unfolded abbreviated_type_defs] :
	"kinding [] (TRecord [(TPrim (Num U16), True), (TPrim (Num U32), False)] Writable) {E}"
	apply (unfold abbreviated_type_defs)?
	apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_5_script \|> EVERY *})
	done

	ML_quiet {*
	val typing_helper_6_script : tac list = [
	(RTac @{thm kind_tprim})
	] *}


	lemma typing_helper_6[unfolded abbreviated_type_defs] :
	"kinding [] (TPrim (Num U8)) {E}"
	apply (unfold abbreviated_type_defs)?
	apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_6_script \|> EVERY *})
	done

	ML_quiet {*
	val typing_helper_7_script : tac list = [
	(RTac @{thm kind_trec[where k = "{E}"]}),
	(RTac @{thm kind_record_cons1}),
	(RTac @{thm typing_helper_6}),
	(RTac @{thm kind_record_cons1}),
	(RTac @{thm typing_helper_1}),
	(RTac @{thm kind_record_empty}),
	(SimpTac ([],[]))
	] *}


	lemma typing_helper_7[unfolded abbreviated_type_defs] :
	"kinding [] abbreviatedType1 {E}"
	apply (unfold abbreviated_type_defs)?
	apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_7_script \|> EVERY *})
	done

	ML_quiet {*
	val typing_helper_8_script : tac list = [
	(RTac @{thm kind_tprim[where k = "{E,S,D}"]})
	] *}


	lemma typing_helper_8[unfolded abbreviated_type_defs] :
	"kinding [] (TPrim (Num U8)) {E, S, D}"
	apply (unfold abbreviated_type_defs)?
	apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_8_script \|> EVERY *})
	done

	ML_quiet {*
	val typing_helper_9_script : tac list = [
	(RTac @{thm kind_trec[where k = "{E}"]}),
	(RTac @{thm kind_record_cons2}),
	(RTac @{thm typing_helper_8}),
	(RTac @{thm kind_record_cons1}),
	(RTac @{thm typing_helper_1}),
	(RTac @{thm kind_record_empty}),
	(SimpTac ([],[]))
	] *}


	lemma typing_helper_9[unfolded abbreviated_type_defs] :
	"kinding [] (TRecord [(TPrim (Num U8), True), (TPrim (Num U16), False)] Writable) {E}"
	apply (unfold abbreviated_type_defs)?
	apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_9_script \|> EVERY *})
	done

	ML_quiet {*
	val foobar_typecorrect_script : hints list = [
	KindingTacs [(RTac @{thm typing_helper_3})],
	KindingTacs [(RTac @{thm typing_helper_3})],
	TypingTacs [],
	KindingTacs [(RTac @{thm typing_helper_4})],
	KindingTacs [(RTac @{thm typing_helper_5})],
	TypingTacs [],
	KindingTacs [(RTac @{thm typing_helper_4})],
	KindingTacs [(RTac @{thm typing_helper_3})],
	TypingTacs [(RTac @{thm typing_put'}),(SplitsTac (4,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_4})]),(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[@{thm Product_Type.prod.inject}])),(RTac @{thm typing_helper_4}),(RTac @{thm disjI2[where Q = "True"]}),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_4}]),(SimpTac ([],[])),(SimpTac ([],[]))],
	TypingTacs []
	] *}


	ML_quiet {*
	val foobar_ttyping_details_future = get_all_typing_details_future @{context} "foobar"
	foobar_typecorrect_script*}


	lemma foobar_typecorrect :
	"\<Xi>, fst foobar_type, (foobar_typetree, [Some (fst (snd foobar_type))]) T\<turnstile> foobar : snd (snd foobar_type)"
	apply (tactic {* resolve_future_typecorrect @{context} foobar_ttyping_details_future *})
	done

	ML_quiet {*
	val foo_typecorrect_script : hints list = [
	KindingTacs [(RTac @{thm typing_helper_7})],
	KindingTacs [(RTac @{thm typing_helper_7})],
	TypingTacs [],
	KindingTacs [(RTac @{thm typing_helper_8})],
	KindingTacs [(RTac @{thm typing_helper_9})],
	TypingTacs [],
	KindingTacs [(RTac @{thm typing_helper_8})],
	KindingTacs [(RTac @{thm typing_helper_7})],
	TypingTacs [(RTac @{thm typing_put'}),(SplitsTac (4,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_8})]),(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_9})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_9}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[@{thm Product_Type.prod.inject}])),(RTac @{thm typing_helper_8}),(RTac @{thm disjI2[where Q = "True"]}),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_8}]),(SimpTac ([],[])),(SimpTac ([],[]))],
	TypingTacs []
	] *}


	ML_quiet {*
	val foo_ttyping_details_future = get_all_typing_details_future @{context} "foo"
	foo_typecorrect_script*}


	lemma foo_typecorrect :
	"\<Xi>, fst foo_type, (foo_typetree, [Some (fst (snd foo_type))]) T\<turnstile> foo : snd (snd foo_type)"
	apply (tactic {* resolve_future_typecorrect @{context} foo_ttyping_details_future *})
	done

	ML_quiet {*
	val (_, foobar_typing_tree, foobar_typing_bucket)
	= Future.join foobar_ttyping_details_future
	*}


	ML_quiet {*
	val (_, foo_typing_tree, foo_typing_bucket)
	= Future.join foo_ttyping_details_future
	*}


	end