c-refinement/tests/FunFun.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)
  *)

 (*
  * Program specifications generated from:
  *   cogent --type-proof=FunFun --fml-typing-tree fun.cogent
  *   cogent -gfun_dsl --infer-c-func=fun.ac fun.cogent && cat fun_dsl.c fun_pp_inferred.c > fun.c
  *)
 theory FunFun
 imports
   "../Cogent_Corres"
   "../TypeProofGen"
   "../Corres_Tac"
   "../Tidy"
 begin

 lemmas abbreviated_type_defs =
   TrueI

 definition
   "abs_type \<equiv> ([], (TUnit, TFun TUnit TUnit))"

 definition
   "i_type \<equiv> ([], (TUnit, TUnit))"

 definition
   "i \<equiv> Let (Var 0) (Var 0)"

 definition
   "i2_type \<equiv> ([], (TUnit, TUnit))"

 definition
   "i2 \<equiv> Let (Var 0) (App (Fun i []) (Var 0))"

 definition
   "f_type \<equiv> ([], (TUnit, TUnit))"

 definition
   "f \<equiv> Let (Var 0) (Let (App (AFun ''abs'' []) (Var 0)) (App (Var 0) (Var 1)))"

 definition
   "\<Xi> func_name' \<equiv> case func_name' of ''abs'' \<Rightarrow> abs_type | ''i'' \<Rightarrow> i_type | ''i2'' \<Rightarrow> i2_type | ''f'' \<Rightarrow> f_type"

 definition
   "\<xi> func_name' \<equiv> case func_name' of ''abs'' \<Rightarrow> undefined"

 definition
   "i_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some TUnit] TyTrLeaf"

 definition
   "i2_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some TUnit] TyTrLeaf"

 definition
   "f_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some TUnit] (TyTrSplit (Cons (Some TSK_S) (Cons None [])) [] TyTrLeaf [Some (TFun TUnit TUnit)] TyTrLeaf)"

 ML {* open TTyping_Tactics *}

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


 lemma typing_helper_1[unfolded abbreviated_type_defs] :
   "kinding [] TUnit {E, S, D}"
   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 = [
 (SimpTac ([],[(nth @{thms HOL.simp_thms} (25-1)),(nth @{thms HOL.simp_thms} (26-1))]))
 ] *}


 lemma typing_helper_2[unfolded abbreviated_type_defs] :
   "list_all2 (kinding []) [] []"
   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_tfun[where k = "{E,S,D}"]}),
 (RTac @{thm typing_helper_1}),
 (RTac @{thm typing_helper_1})
 ] *}


 lemma typing_helper_3[unfolded abbreviated_type_defs] :
   "kinding [] (TFun TUnit TUnit) {E, S, D}"
   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_tfun[where k = "{E,S,D}"]}),
 (RTac @{thm typing_helper_1}),
 (RTac @{thm typing_helper_3})
 ] *}


 lemma typing_helper_4[unfolded abbreviated_type_defs] :
   "kinding [] (TFun TUnit (TFun TUnit TUnit)) {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 i_typecorrect_script : hints list = [
 KindingTacs [(RTac @{thm typing_helper_1})],
 KindingTacs [(RTac @{thm typing_helper_1})],
 TypingTacs [],
 TypingTacs []
 ] *}


 ML_quiet {*
 val i_ttyping_details_future = get_all_typing_details_future @{context} "i"
    i_typecorrect_script*}


 lemma i_typecorrect :
   "\<Xi>, fst i_type, (i_typetree, [Some (fst (snd i_type))]) T\<turnstile> i : snd (snd i_type)"
   apply (tactic {* resolve_future_typecorrect @{context} i_ttyping_details_future *})
   done

 ML_quiet {*
 val i2_typecorrect_script : hints list = [
 KindingTacs [(RTac @{thm typing_helper_1})],
 KindingTacs [(RTac @{thm typing_helper_1})],
 TypingTacs [],
 TypingTacs [(RTac @{thm typing_app}),(SplitsTac (2,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_1})])])),(RTac @{thm typing_fun'}),(RTac @{thm i_typecorrect[simplified i_type_def i_typetree_def, simplified]}),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_1}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[]))]
 ] *}


 ML_quiet {*
 val i2_ttyping_details_future = get_all_typing_details_future @{context} "i2"
    i2_typecorrect_script*}


 lemma i2_typecorrect :
   "\<Xi>, fst i2_type, (i2_typetree, [Some (fst (snd i2_type))]) T\<turnstile> i2 : snd (snd i2_type)"
   apply (tactic {* resolve_future_typecorrect @{context} i2_ttyping_details_future *})
   done

 ML_quiet {*
 val f_typecorrect_script : hints list = [
 KindingTacs [(RTac @{thm typing_helper_1})],
 KindingTacs [(RTac @{thm typing_helper_1})],
 TypingTacs [],
 KindingTacs [(RTac @{thm typing_helper_3})],
 TypingTacs [(RTac @{thm typing_app}),(SplitsTac (2,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_1})])])),(RTac @{thm typing_afun'}),(SimpTac ([@{thm \<Xi>_def},@{thm abs_type_def}],[])),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_4}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[]))],
 TypingTacs [(RTac @{thm typing_app}),(SplitsTac (3,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})]),(1,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_1})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[]))]
 ] *}


 ML_quiet {*
 val f_ttyping_details_future = get_all_typing_details_future @{context} "f"
    f_typecorrect_script*}


 lemma f_typecorrect :
   "\<Xi>, fst f_type, (f_typetree, [Some (fst (snd f_type))]) T\<turnstile> f : snd (snd f_type)"
   apply (tactic {* resolve_future_typecorrect @{context} f_ttyping_details_future *})
   done

 ML_quiet {*
 val (_, i_typing_tree, i_typing_bucket)
 = Future.join i_ttyping_details_future
 *}


 ML_quiet {*
 val (_, i2_typing_tree, i2_typing_bucket)
 = Future.join i2_ttyping_details_future
 *}


 ML_quiet {*
 val (_, f_typing_tree, f_typing_bucket)
 = Future.join f_ttyping_details_future
 *}


 new_C_include_dir "../../cogent/tests"
 install_C_file "fun.c"
 autocorres [ts_rules = nondet, no_opt, skip_word_abs] "fun.c"

 instantiation bool_t_C :: cogent_C_val
 begin
 definition type_rel_bool_t_C_def:
   "type_rel typ (_ :: bool_t_C itself) \<equiv> (typ = RPrim Bool)"

 definition val_rel_bool_t_C_def:
   "val_rel uv (x :: bool_t_C) \<equiv> uv = UPrim (LBool (bool_t_C.boolean_C x \<noteq> 0))"
 instance ..
 end

 instantiation unit_t_C :: cogent_C_val begin
   definition type_rel_unit_t_C: "type_rel r (_ :: unit_t_C itself) \<equiv> r = RUnit"
   definition val_rel_unit_t_C: "val_rel uv (_ :: unit_t_C) \<equiv> uv = UUnit"
   instance ..
 end


 (* [abs, f] is a non-terminating program, so we cannot prove correspondence. *)
 context "fun" begin
   thm abs'_def
   thm f'.simps dispatch_t1'.simps
 end


 (* [i, i2] is a terminating program. *)
 locale fun_u_sem = "fun" + update_sem_init
 begin

 local_setup {* fold tidy_C_fun_def' ["i", "i2"] *}
 thm i_def i'_def' i2_def i2'_def'

 lemmas corres_nested_let = TrueI (* unused *)

 lemma i_corres: "val_rel a a' \<Longrightarrow> corres srel i (i' a') \<xi> [a] \<Xi> [Some TUnit] \<sigma> s"
   apply (tactic {* corres_tac @{context}
     (peel_two i_typing_tree)
     @{thms i_def i'_def' i_type_def abbreviated_type_defs} [] []
     @{thm TrueI} [] [] [] [] @{thm LETBANG_TRUE_def} [] true *})
   done

 lemma i2_corres: "val_rel a a' \<Longrightarrow> corres srel i2 (i2' a') \<xi> [a] \<Xi> [Some TUnit] \<sigma> s"
   apply (tactic {* corres_tac @{context}
     (peel_two i2_typing_tree)
     @{thms i2_def i2'_def' i2_type_def abbreviated_type_defs} [] @{thms i_corres}
     @{thm TrueI} [] [] [] [] @{thm LETBANG_TRUE_def} [] true *})
   done

 end

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

	(*
	* Program specifications generated from:
	* cogent --type-proof=FunFun --fml-typing-tree fun.cogent
	* cogent -gfun_dsl --infer-c-func=fun.ac fun.cogent && cat fun_dsl.c fun_pp_inferred.c > fun.c
	*)
	theory FunFun
	imports
	"../Cogent_Corres"
	"../TypeProofGen"
	"../Corres_Tac"
	"../Tidy"
	begin

	lemmas abbreviated_type_defs =
	TrueI

	definition
	"abs_type \<equiv> ([], (TUnit, TFun TUnit TUnit))"

	definition
	"i_type \<equiv> ([], (TUnit, TUnit))"

	definition
	"i \<equiv> Let (Var 0) (Var 0)"

	definition
	"i2_type \<equiv> ([], (TUnit, TUnit))"

	definition
	"i2 \<equiv> Let (Var 0) (App (Fun i []) (Var 0))"

	definition
	"f_type \<equiv> ([], (TUnit, TUnit))"

	definition
	"f \<equiv> Let (Var 0) (Let (App (AFun ''abs'' []) (Var 0)) (App (Var 0) (Var 1)))"

	definition
	"\<Xi> func_name' \<equiv> case func_name' of ''abs'' \<Rightarrow> abs_type \| ''i'' \<Rightarrow> i_type \| ''i2'' \<Rightarrow> i2_type \| ''f'' \<Rightarrow> f_type"

	definition
	"\<xi> func_name' \<equiv> case func_name' of ''abs'' \<Rightarrow> undefined"

	definition
	"i_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some TUnit] TyTrLeaf"

	definition
	"i2_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some TUnit] TyTrLeaf"

	definition
	"f_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some TUnit] (TyTrSplit (Cons (Some TSK_S) (Cons None [])) [] TyTrLeaf [Some (TFun TUnit TUnit)] TyTrLeaf)"

	ML {* open TTyping_Tactics *}

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


	lemma typing_helper_1[unfolded abbreviated_type_defs] :
	"kinding [] TUnit {E, S, D}"
	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 = [
	(SimpTac ([],[(nth @{thms HOL.simp_thms} (25-1)),(nth @{thms HOL.simp_thms} (26-1))]))
	] *}


	lemma typing_helper_2[unfolded abbreviated_type_defs] :
	"list_all2 (kinding []) [] []"
	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_tfun[where k = "{E,S,D}"]}),
	(RTac @{thm typing_helper_1}),
	(RTac @{thm typing_helper_1})
	] *}


	lemma typing_helper_3[unfolded abbreviated_type_defs] :
	"kinding [] (TFun TUnit TUnit) {E, S, D}"
	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_tfun[where k = "{E,S,D}"]}),
	(RTac @{thm typing_helper_1}),
	(RTac @{thm typing_helper_3})
	] *}


	lemma typing_helper_4[unfolded abbreviated_type_defs] :
	"kinding [] (TFun TUnit (TFun TUnit TUnit)) {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 i_typecorrect_script : hints list = [
	KindingTacs [(RTac @{thm typing_helper_1})],
	KindingTacs [(RTac @{thm typing_helper_1})],
	TypingTacs [],
	TypingTacs []
	] *}


	ML_quiet {*
	val i_ttyping_details_future = get_all_typing_details_future @{context} "i"
	i_typecorrect_script*}


	lemma i_typecorrect :
	"\<Xi>, fst i_type, (i_typetree, [Some (fst (snd i_type))]) T\<turnstile> i : snd (snd i_type)"
	apply (tactic {* resolve_future_typecorrect @{context} i_ttyping_details_future *})
	done

	ML_quiet {*
	val i2_typecorrect_script : hints list = [
	KindingTacs [(RTac @{thm typing_helper_1})],
	KindingTacs [(RTac @{thm typing_helper_1})],
	TypingTacs [],
	TypingTacs [(RTac @{thm typing_app}),(SplitsTac (2,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_1})])])),(RTac @{thm typing_fun'}),(RTac @{thm i_typecorrect[simplified i_type_def i_typetree_def, simplified]}),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_1}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[]))]
	] *}


	ML_quiet {*
	val i2_ttyping_details_future = get_all_typing_details_future @{context} "i2"
	i2_typecorrect_script*}


	lemma i2_typecorrect :
	"\<Xi>, fst i2_type, (i2_typetree, [Some (fst (snd i2_type))]) T\<turnstile> i2 : snd (snd i2_type)"
	apply (tactic {* resolve_future_typecorrect @{context} i2_ttyping_details_future *})
	done

	ML_quiet {*
	val f_typecorrect_script : hints list = [
	KindingTacs [(RTac @{thm typing_helper_1})],
	KindingTacs [(RTac @{thm typing_helper_1})],
	TypingTacs [],
	KindingTacs [(RTac @{thm typing_helper_3})],
	TypingTacs [(RTac @{thm typing_app}),(SplitsTac (2,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_1})])])),(RTac @{thm typing_afun'}),(SimpTac ([@{thm \<Xi>_def},@{thm abs_type_def}],[])),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_4}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[]))],
	TypingTacs [(RTac @{thm typing_app}),(SplitsTac (3,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})]),(1,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_1})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[]))]
	] *}


	ML_quiet {*
	val f_ttyping_details_future = get_all_typing_details_future @{context} "f"
	f_typecorrect_script*}


	lemma f_typecorrect :
	"\<Xi>, fst f_type, (f_typetree, [Some (fst (snd f_type))]) T\<turnstile> f : snd (snd f_type)"
	apply (tactic {* resolve_future_typecorrect @{context} f_ttyping_details_future *})
	done

	ML_quiet {*
	val (_, i_typing_tree, i_typing_bucket)
	= Future.join i_ttyping_details_future
	*}


	ML_quiet {*
	val (_, i2_typing_tree, i2_typing_bucket)
	= Future.join i2_ttyping_details_future
	*}


	ML_quiet {*
	val (_, f_typing_tree, f_typing_bucket)
	= Future.join f_ttyping_details_future
	*}


	new_C_include_dir "../../cogent/tests"
	install_C_file "fun.c"
	autocorres [ts_rules = nondet, no_opt, skip_word_abs] "fun.c"

	instantiation bool_t_C :: cogent_C_val
	begin
	definition type_rel_bool_t_C_def:
	"type_rel typ (_ :: bool_t_C itself) \<equiv> (typ = RPrim Bool)"

	definition val_rel_bool_t_C_def:
	"val_rel uv (x :: bool_t_C) \<equiv> uv = UPrim (LBool (bool_t_C.boolean_C x \<noteq> 0))"
	instance ..
	end

	instantiation unit_t_C :: cogent_C_val begin
	definition type_rel_unit_t_C: "type_rel r (_ :: unit_t_C itself) \<equiv> r = RUnit"
	definition val_rel_unit_t_C: "val_rel uv (_ :: unit_t_C) \<equiv> uv = UUnit"
	instance ..
	end


	(* [abs, f] is a non-terminating program, so we cannot prove correspondence. *)
	context "fun" begin
	thm abs'_def
	thm f'.simps dispatch_t1'.simps
	end


	(* [i, i2] is a terminating program. *)
	locale fun_u_sem = "fun" + update_sem_init
	begin

	local_setup {* fold tidy_C_fun_def' ["i", "i2"] *}
	thm i_def i'_def' i2_def i2'_def'

	lemmas corres_nested_let = TrueI (* unused *)

	lemma i_corres: "val_rel a a' \<Longrightarrow> corres srel i (i' a') \<xi> [a] \<Xi> [Some TUnit] \<sigma> s"
	apply (tactic {* corres_tac @{context}
	(peel_two i_typing_tree)
	@{thms i_def i'_def' i_type_def abbreviated_type_defs} [] []
	@{thm TrueI} [] [] [] [] @{thm LETBANG_TRUE_def} [] true *})
	done

	lemma i2_corres: "val_rel a a' \<Longrightarrow> corres srel i2 (i2' a') \<xi> [a] \<Xi> [Some TUnit] \<sigma> s"
	apply (tactic {* corres_tac @{context}
	(peel_two i2_typing_tree)
	@{thms i2_def i2'_def' i2_type_def abbreviated_type_defs} [] @{thms i_corres}
	@{thm TrueI} [] [] [] [] @{thm LETBANG_TRUE_def} [] true *})
	done

	end

	end