isabelle: src/HOL/SizeChange/Examples.thy@4dc278c8dc59 (annotated)

25314 5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	1	(* Title: HOL/Library/SCT_Examples.thy
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	2	ID: $Id$
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	3	Author: Alexander Krauss, TU Muenchen
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	4	*)
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	5
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	6	header {* Examples for Size-Change Termination *}
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	7
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	8	theory Examples
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	9	imports Size_Change_Termination
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	10	begin
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	11
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	12	function f :: "nat \<Rightarrow> nat \<Rightarrow> nat"
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	13	where
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	14	"f n 0 = n"
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	15	\| "f 0 (Suc m) = f (Suc m) m"
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	16	\| "f (Suc n) (Suc m) = f m n"
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	17	by pat_completeness auto
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	18
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	19
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	20	termination
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	21	unfolding f_rel_def lfp_const
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	22	apply (rule SCT_on_relations)
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	23	apply (tactic "Sct.abs_rel_tac") (* Build call descriptors *)
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	24	apply (rule ext, rule ext, simp) (* Show that they are correct *)
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: 26822 diff changeset	25	apply (tactic "Sct.mk_call_graph @{context}") (* Build control graph *)
25314 5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	26	apply (rule SCT_Main) (* Apply main theorem *)
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	27	apply (simp add:finite_acg_simps) (* show finiteness *)
26822 67c24cfa8def Temporarily disabled invocations of new code generator that do no berghofe parents: 25314 diff changeset	28	oops (FIXME by eval) (* Evaluate to true *)
25314 5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	29
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	30	function p :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	31	where
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	32	"p m n r = (if r>0 then p m (r - 1) n else
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	33	if n>0 then p r (n - 1) m
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	34	else m)"
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	35	by pat_completeness auto
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	36
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	37	termination
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	38	unfolding p_rel_def lfp_const
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	39	apply (rule SCT_on_relations)
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	40	apply (tactic "Sct.abs_rel_tac")
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	41	apply (rule ext, rule ext, simp)
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: 26822 diff changeset	42	apply (tactic "Sct.mk_call_graph @{context}")
25314 5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	43	apply (rule SCT_Main)
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	44	apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
26822 67c24cfa8def Temporarily disabled invocations of new code generator that do no berghofe parents: 25314 diff changeset	45	oops (* FIXME by eval *)
25314 5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	46
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	47	function foo :: "bool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	48	where
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	49	"foo True (Suc n) m = foo True n (Suc m)"
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	50	\| "foo True 0 m = foo False 0 m"
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	51	\| "foo False n (Suc m) = foo False (Suc n) m"
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	52	\| "foo False n 0 = n"
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	53	by pat_completeness auto
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	54
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	55	termination
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	56	unfolding foo_rel_def lfp_const
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	57	apply (rule SCT_on_relations)
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	58	apply (tactic "Sct.abs_rel_tac")
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	59	apply (rule ext, rule ext, simp)
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: 26822 diff changeset	60	apply (tactic "Sct.mk_call_graph @{context}")
25314 5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	61	apply (rule SCT_Main)
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	62	apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
26822 67c24cfa8def Temporarily disabled invocations of new code generator that do no berghofe parents: 25314 diff changeset	63	oops (* FIXME by eval *)
25314 5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	64
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	65
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	66	function (sequential)
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	67	bar :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	68	where
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	69	"bar 0 (Suc n) m = bar m m m"
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	70	\| "bar k n m = 0"
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	71	by pat_completeness auto
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	72
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	73	termination
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	74	unfolding bar_rel_def lfp_const
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	75	apply (rule SCT_on_relations)
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	76	apply (tactic "Sct.abs_rel_tac")
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	77	apply (rule ext, rule ext, simp)
26875 e18574413bc4 Measure functions can now be declared via special rules, allowing for a krauss parents: 26822 diff changeset	78	apply (tactic "Sct.mk_call_graph @{context}")
25314 5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	79	apply (rule SCT_Main)
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	80	apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	81	by (simp only:sctTest_simps cong: sctTest_congs)
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	82
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: diff changeset	83	end

author	ballarin
	Fri, 19 Dec 2008 16:39:23 +0100
changeset 29249	4dc278c8dc59
parent 26875	e18574413bc4
permissions	-rw-r--r--