(*
 * 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